Inference at * 2 0 0 0 
Iof proof for Lemma before last:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  ((x = last(v)))  x before last(v)  v
  x:T. (x  [u / v])  ((x = last([u / v])))  x before last([u / v])  [u / v] 

latex

 by PERMUTE{1:n,
 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{1:n,
 by PERMUTE{18:n} 

latex

 1: .....wf..... NILNIL

 1:   T  Type
 2: .....wf..... NILNIL

 2:   (x.(x  [u / v])  ((x = last([u / v])))  [x; last([u / v])]  [u / v])  T
 3: .....wf..... NILNIL

 3:   (x.(x  [u / v])
 3:   ( ((x = last([u / v])))
 3:   ( ((x = u & [last([u / v])]  v)  [x; last([u / v])]  v))
 3:    T
 4: .....wf..... NILNIL

 4:   T = T
 5: .....wf..... NILNIL

 5: 6. x : T
 5:   (x  [u / v])  
 6: .....wf..... NILNIL

 6: 6. x : T
 6:   (((x = last([u / v])))  [x; last([u / v])]  [u / v])  
 7: .....wf..... NILNIL

 7: 6. x : T
 7:   (((x = last([u / v])))  ((x = u & [last([u / v])]  v)  [x; last([u / v])]  v))  
 8: .....wf..... NILNIL

 8: 6. x : T
 8:   (x  [u / v]) = (x  [u / v])
 9: .....wf..... NILNIL

 9: 6. x : T
 9:   ((x = last([u / v])))  
 10: .....wf..... NILNIL

 10: 6. x : T
 10:   [x; last([u / v])]  [u / v]  
 11: .....wf..... NILNIL

 11: 6. x : T
 11:   ((x = u & [last([u / v])]  v)  [x; last([u / v])]  v)  
 12: .....wf..... NILNIL

 12: 6. x : T
 12:   ((x = last([u / v]))) = ((x = last([u / v])))
 13: .....wf..... NILNIL

 13: 6. T
 13:   T  Type
 14: .....wf..... NILNIL

 14: 6. x : T
 14:   x  T
 15: .....wf..... NILNIL

 15: 6. T
 15:   u  T
 16: .....wf..... NILNIL

 16: 6. T
 16:   [last([u / v])]  (T List)
 17: .....wf..... NILNIL

 17: 6. T
 17:   v  (T List)
 18: 

 18:   x:T.
 18:   (x  [u / v])
 18:    ((x = last([u / v])))
 18:    ((x = u & [last([u / v])]  v)  [x; last([u / v])]  v)
 .

Definitions	t  T, x:A  B(x), x.A(x), f(a), , x:AB(x), P  Q, [], L1  L2, [car / cdr], last(L), s = t, A, (x  l), type List, Type, {T}, x(s), x. t(x), P  Q, P & Q, P  Q, x before y  l, P  Q, x:A. B(x)
Lemmas	cons sublist cons, implies functionality wrt iff, all functionality wrt iff